

LEMMA

tpp implies pp.
=============================
Step 1

? (all x (all y ((tpp x y) => (pp x y))))


> revsk
=============================
Step 2

? ((~ (tpp c651463 c651462)) v (pp c651463 c651462))


> hypdisj
=============================
Step 3

? (pp c651463 c651462)

1. (tpp c651463 c651462)

> ((pp X Y) <-- (tpp X Y))
=============================
Step 4

? (tpp c651463 c651462)

1. (~ (pp c651463 c651462))
2. (tpp c651463 c651462)

> hyp


LEMMA

pp implies p.
=============================
Step 1

? (all x (all y ((pp x y) => (p x y))))


> revsk
=============================
Step 2

? ((~ (pp c656945 c656944)) v (p c656945 c656944))


> hypdisj
=============================
Step 3

? (p c656945 c656944)

1. (pp c656945 c656944)

> ((p X Y) <-- (pp X Y))
=============================
Step 4

? (pp c656945 c656944)

1. (~ (p c656945 c656944))
2. (pp c656945 c656944)

> hyp


LEMMA

Equality transports parthood.
=============================
Step 1

? (all x (all y (all z (((e= x y) & (p z x)) => (p z y)))))


> revsk
=============================
Step 2

? (((~ (e= c662485 c662484)) v (~ (p c662483 c662485))) v (p c662483 c662484))


> hypdisj
=============================
Step 3

? (p c662483 c662484)

1. (p c662483 c662485)
2. (e= c662485 c662484)

> ((p Z X) <-- (~ (c (f656971 Z X Y) Z)))
=============================
Step 4

? (~ (c (f656971 c662483 c662484 Var35) c662483))

1. (~ (p c662483 c662484))
2. (p c662483 c662485)
3. (e= c662485 c662484)

> ((~ (c Y X)) <-- (p X Z) (~ (c Y Z)))
|=============================
|Step 5
|
|? (p c662483 Var38)
|
|1. (c (f656971 c662483 c662484 Var35) c662483)
|2. (~ (p c662483 c662484))
|3. (p c662483 c662485)
|4. (e= c662485 c662484)
|
|> hyp
=============================
Step 6

? (~ (c (f656971 c662483 c662484 Var35) c662485))

1. (c (f656971 c662483 c662484 Var35) c662483)
2. (~ (p c662483 c662484))
3. (p c662483 c662485)
4. (e= c662485 c662484)

> ((~ (c Y X)) <-- (p X Z) (~ (c Y Z)))
|=============================
|Step 7
|
|? (p c662485 Var42)
|
|1. (c (f656971 c662483 c662484 Var35) c662485)
|2. (c (f656971 c662483 c662484 Var35) c662483)
|3. (~ (p c662483 c662484))
|4. (p c662483 c662485)
|5. (e= c662485 c662484)
|
|> ((p X Y) <-- (e= X Y))
|=============================
|Step 8
|
|? (e= c662485 Var42)
|
|1. (~ (p c662485 Var42))
|2. (c (f656971 c662483 c662484 Var35) c662485)
|3. (c (f656971 c662483 c662484 Var35) c662483)
|4. (~ (p c662483 c662484))
|5. (p c662483 c662485)
|6. (e= c662485 c662484)
|
|> hyp
=============================
Step 9

? (~ (c (f656971 c662483 c662484 Var35) c662484))

1. (c (f656971 c662483 c662484 Var35) c662485)
2. (c (f656971 c662483 c662484 Var35) c662483)
3. (~ (p c662483 c662484))
4. (p c662483 c662485)
5. (e= c662485 c662484)

> ((~ (c (f656971 Y Z X) Z)) <-- (~ (p Y Z)))
=============================
Step 10

? (~ (p c662483 c662484))

1. (c (f656971 c662483 c662484 Var35) c662484)
2. (c (f656971 c662483 c662484 Var35) c662485)
3. (c (f656971 c662483 c662484 Var35) c662483)
4. (~ (p c662483 c662484))
5. (p c662483 c662485)
6. (e= c662485 c662484)

> hyp


LEMMA

Equality transports external connection.
=============================
Step 1

? (all x (all y (all z (((e= x y) & (ec z x)) => (ec z y)))))


> revsk
=============================
Step 2

? (((~ (e= c668181 c668180)) v (~ (ec c668179 c668181))) v (ec c668179 c668180))


> hypdisj
=============================
Step 3

? (ec c668179 c668180)

1. (ec c668179 c668181)
2. (e= c668181 c668180)

> ((ec X Y) <-- (c X Y) (~ (o X Y)))
|=============================
|Step 4
|
|? (c c668179 c668180)
|
|1. (~ (ec c668179 c668180))
|2. (ec c668179 c668181)
|3. (e= c668181 c668180)
|
|> ((c Y X) <-- (p Z X) (c Y Z))
||=============================
||Step 5
||
||? (p Var63 c668180)
||
||1. (~ (c c668179 c668180))
||2. (~ (ec c668179 c668180))
||3. (ec c668179 c668181)
||4. (e= c668181 c668180)
||
||> ((p Z X) <-- (~ (c (f662517 Z X Y) Z)))
||=============================
||Step 6
||
||? (~ (c (f662517 Var63 c668180 Var66) Var63))
||
||1. (~ (p Var63 c668180))
||2. (~ (c c668179 c668180))
||3. (~ (ec c668179 c668180))
||4. (ec c668179 c668181)
||5. (e= c668181 c668180)
||
||> ((~ (c Y X)) <-- (p X Z) (~ (c Y Z)))
|||=============================
|||Step 7
|||
|||? (p Var63 Var69)
|||
|||1. (c (f662517 Var63 c668180 Var66) Var63)
|||2. (~ (p Var63 c668180))
|||3. (~ (c c668179 c668180))
|||4. (~ (ec c668179 c668180))
|||5. (ec c668179 c668181)
|||6. (e= c668181 c668180)
|||
|||> ((p X Y) <-- (e= X Y))
|||=============================
|||Step 8
|||
|||? (e= Var63 Var69)
|||
|||1. (~ (p Var63 Var69))
|||2. (c (f662517 Var63 c668180 Var66) Var63)
|||3. (~ (p Var63 c668180))
|||4. (~ (c c668179 c668180))
|||5. (~ (ec c668179 c668180))
|||6. (ec c668179 c668181)
|||7. (e= c668181 c668180)
|||
|||> hyp
||=============================
||Step 9
||
||? (~ (c (f662517 c668181 c668180 Var66) c668180))
||
||1. (c (f662517 c668181 c668180 Var66) c668181)
||2. (~ (p c668181 c668180))
||3. (~ (c c668179 c668180))
||4. (~ (ec c668179 c668180))
||5. (ec c668179 c668181)
||6. (e= c668181 c668180)
||
||> ((~ (c (f662517 Y Z X) Z)) <-- (~ (p Y Z)))
||=============================
||Step 10
||
||? (~ (p c668181 c668180))
||
||1. (c (f662517 c668181 c668180 Var66) c668180)
||2. (c (f662517 c668181 c668180 Var66) c668181)
||3. (~ (p c668181 c668180))
||4. (~ (c c668179 c668180))
||5. (~ (ec c668179 c668180))
||6. (ec c668179 c668181)
||7. (e= c668181 c668180)
||
||> hyp
|=============================
|Step 11
|
|? (c c668179 c668181)
|
|1. (~ (c c668179 c668180))
|2. (~ (ec c668179 c668180))
|3. (ec c668179 c668181)
|4. (e= c668181 c668180)
|
|> ((c X Y) <-- (ec X Y))
|=============================
|Step 12
|
|? (ec c668179 c668181)
|
|1. (~ (c c668179 c668181))
|2. (~ (c c668179 c668180))
|3. (~ (ec c668179 c668180))
|4. (ec c668179 c668181)
|5. (e= c668181 c668180)
|
|> hyp
=============================
Step 13

? (~ (o c668179 c668180))

1. (~ (ec c668179 c668180))
2. (ec c668179 c668181)
3. (e= c668181 c668180)

> ((~ (o X Y)) <-- (~ (p (f662543 X Y) Y)))
=============================
Step 14

? (~ (p (f662543 c668179 c668180) c668180))

1. (o c668179 c668180)
2. (~ (ec c668179 c668180))
3. (ec c668179 c668181)
4. (e= c668181 c668180)

> ((~ (p Y X)) <-- (e= X Z) (~ (p Y Z)))
|=============================
|Step 15
|
|? (e= c668180 Var83)
|
|1. (p (f662543 c668179 c668180) c668180)
|2. (o c668179 c668180)
|3. (~ (ec c668179 c668180))
|4. (ec c668179 c668181)
|5. (e= c668181 c668180)
|
|> ((e= Y X) <-- (p Y X) (p X Y))
||=============================
||Step 16
||
||? (p c668180 Var83)
||
||1. (~ (e= c668180 Var83))
||2. (p (f662543 c668179 c668180) c668180)
||3. (o c668179 c668180)
||4. (~ (ec c668179 c668180))
||5. (ec c668179 c668181)
||6. (e= c668181 c668180)
||
||> ((p Y X) <-- (e= X Y))
||=============================
||Step 17
||
||? (e= Var83 c668180)
||
||1. (~ (p c668180 Var83))
||2. (~ (e= c668180 Var83))
||3. (p (f662543 c668179 c668180) c668180)
||4. (o c668179 c668180)
||5. (~ (ec c668179 c668180))
||6. (ec c668179 c668181)
||7. (e= c668181 c668180)
||
||> hyp
|=============================
|Step 18
|
|? (p c668181 c668180)
|
|1. (~ (e= c668180 c668181))
|2. (p (f662543 c668179 c668180) c668180)
|3. (o c668179 c668180)
|4. (~ (ec c668179 c668180))
|5. (ec c668179 c668181)
|6. (e= c668181 c668180)
|
|> ((p X Y) <-- (e= X Y))
|=============================
|Step 19
|
|? (e= c668181 c668180)
|
|1. (~ (p c668181 c668180))
|2. (~ (e= c668180 c668181))
|3. (p (f662543 c668179 c668180) c668180)
|4. (o c668179 c668180)
|5. (~ (ec c668179 c668180))
|6. (ec c668179 c668181)
|7. (e= c668181 c668180)
|
|> hyp
=============================
Step 20

? (~ (p (f662543 c668179 c668180) c668181))

1. (p (f662543 c668179 c668180) c668180)
2. (o c668179 c668180)
3. (~ (ec c668179 c668180))
4. (ec c668179 c668181)
5. (e= c668181 c668180)

> ((~ (p X Z)) <-- (p X Y) (~ (o Y Z)))
|=============================
|Step 21
|
|? (p (f662543 c668179 c668180) c668179)
|
|1. (p (f662543 c668179 c668180) c668181)
|2. (p (f662543 c668179 c668180) c668180)
|3. (o c668179 c668180)
|4. (~ (ec c668179 c668180))
|5. (ec c668179 c668181)
|6. (e= c668181 c668180)
|
|> ((p (f662543 X Y) X) <-- (o X Y))
|=============================
|Step 22
|
|? (o c668179 c668180)
|
|1. (~ (p (f662543 c668179 c668180) c668179))
|2. (p (f662543 c668179 c668180) c668181)
|3. (p (f662543 c668179 c668180) c668180)
|4. (o c668179 c668180)
|5. (~ (ec c668179 c668180))
|6. (ec c668179 c668181)
|7. (e= c668181 c668180)
|
|> hyp
=============================
Step 23

? (~ (o c668179 c668181))

1. (p (f662543 c668179 c668180) c668181)
2. (p (f662543 c668179 c668180) c668180)
3. (o c668179 c668180)
4. (~ (ec c668179 c668180))
5. (ec c668179 c668181)
6. (e= c668181 c668180)

> ((~ (o X Y)) <-- (ec X Y))
=============================
Step 24

? (ec c668179 c668181)

1. (o c668179 c668181)
2. (p (f662543 c668179 c668180) c668181)
3. (p (f662543 c668179 c668180) c668180)
4. (o c668179 c668180)
5. (~ (ec c668179 c668180))
6. (ec c668179 c668181)
7. (e= c668181 c668180)

> hyp


LEMMA

From tpp(x,y) and e=(y,z), derive pp(x,z).
=============================
Step 1

? (all x (all y (all z (((tpp x y) & (e= y z)) => (pp x z)))))


> revsk
=============================
Step 2

? (((~ (tpp c674033 c674032)) v (~ (e= c674032 c674031))) v (pp c674033 c674031))


> hypdisj
=============================
Step 3

? (pp c674033 c674031)

1. (e= c674032 c674031)
2. (tpp c674033 c674032)

> ((pp Y X) <-- (p Y X) (~ (p X Y)))
|=============================
|Step 4
|
|? (p c674033 c674031)
|
|1. (~ (pp c674033 c674031))
|2. (e= c674032 c674031)
|3. (tpp c674033 c674032)
|
|> ((p Z X) <-- (~ (c (f668219 Z X Y) Z)))
|=============================
|Step 5
|
|? (~ (c (f668219 c674033 c674031 Var65) c674033))
|
|1. (~ (p c674033 c674031))
|2. (~ (pp c674033 c674031))
|3. (e= c674032 c674031)
|4. (tpp c674033 c674032)
|
|> ((~ (c Y X)) <-- (p X Z) (~ (c Y Z)))
||=============================
||Step 6
||
||? (p c674033 Var68)
||
||1. (c (f668219 c674033 c674031 Var65) c674033)
||2. (~ (p c674033 c674031))
||3. (~ (pp c674033 c674031))
||4. (e= c674032 c674031)
||5. (tpp c674033 c674032)
||
||> ((p X Y) <-- (pp X Y))
||=============================
||Step 7
||
||? (pp c674033 Var68)
||
||1. (~ (p c674033 Var68))
||2. (c (f668219 c674033 c674031 Var65) c674033)
||3. (~ (p c674033 c674031))
||4. (~ (pp c674033 c674031))
||5. (e= c674032 c674031)
||6. (tpp c674033 c674032)
||
||> ((pp X Y) <-- (tpp X Y))
||=============================
||Step 8
||
||? (tpp c674033 Var68)
||
||1. (~ (pp c674033 Var68))
||2. (~ (p c674033 Var68))
||3. (c (f668219 c674033 c674031 Var65) c674033)
||4. (~ (p c674033 c674031))
||5. (~ (pp c674033 c674031))
||6. (e= c674032 c674031)
||7. (tpp c674033 c674032)
||
||> hyp
|=============================
|Step 9
|
|? (~ (c (f668219 c674033 c674031 Var65) c674032))
|
|1. (c (f668219 c674033 c674031 Var65) c674033)
|2. (~ (p c674033 c674031))
|3. (~ (pp c674033 c674031))
|4. (e= c674032 c674031)
|5. (tpp c674033 c674032)
|
|> ((~ (c Y X)) <-- (p X Z) (~ (c Y Z)))
||=============================
||Step 10
||
||? (p c674032 Var76)
||
||1. (c (f668219 c674033 c674031 Var65) c674032)
||2. (c (f668219 c674033 c674031 Var65) c674033)
||3. (~ (p c674033 c674031))
||4. (~ (pp c674033 c674031))
||5. (e= c674032 c674031)
||6. (tpp c674033 c674032)
||
||> ((p X Y) <-- (e= X Y))
||=============================
||Step 11
||
||? (e= c674032 Var76)
||
||1. (~ (p c674032 Var76))
||2. (c (f668219 c674033 c674031 Var65) c674032)
||3. (c (f668219 c674033 c674031 Var65) c674033)
||4. (~ (p c674033 c674031))
||5. (~ (pp c674033 c674031))
||6. (e= c674032 c674031)
||7. (tpp c674033 c674032)
||
||> hyp
|=============================
|Step 12
|
|? (~ (c (f668219 c674033 c674031 Var65) c674031))
|
|1. (c (f668219 c674033 c674031 Var65) c674032)
|2. (c (f668219 c674033 c674031 Var65) c674033)
|3. (~ (p c674033 c674031))
|4. (~ (pp c674033 c674031))
|5. (e= c674032 c674031)
|6. (tpp c674033 c674032)
|
|> ((~ (c (f668219 Y Z X) Z)) <-- (~ (p Y Z)))
|=============================
|Step 13
|
|? (~ (p c674033 c674031))
|
|1. (c (f668219 c674033 c674031 Var65) c674031)
|2. (c (f668219 c674033 c674031 Var65) c674032)
|3. (c (f668219 c674033 c674031 Var65) c674033)
|4. (~ (p c674033 c674031))
|5. (~ (pp c674033 c674031))
|6. (e= c674032 c674031)
|7. (tpp c674033 c674032)
|
|> hyp
=============================
Step 14

? (~ (p c674031 c674033))

1. (~ (pp c674033 c674031))
2. (e= c674032 c674031)
3. (tpp c674033 c674032)

> ((~ (p X Y)) <-- (p Y X) (~ (e= X Y)))
|=============================
|Step 15
|
|? (p c674033 c674031)
|
|1. (p c674031 c674033)
|2. (~ (pp c674033 c674031))
|3. (e= c674032 c674031)
|4. (tpp c674033 c674032)
|
|> ((p Y X) <-- (e= Z X) (p Y Z))
||=============================
||Step 16
||
||? (e= Var87 c674031)
||
||1. (~ (p c674033 c674031))
||2. (p c674031 c674033)
||3. (~ (pp c674033 c674031))
||4. (e= c674032 c674031)
||5. (tpp c674033 c674032)
||
||> hyp
|=============================
|Step 17
|
|? (p c674033 c674032)
|
|1. (~ (p c674033 c674031))
|2. (p c674031 c674033)
|3. (~ (pp c674033 c674031))
|4. (e= c674032 c674031)
|5. (tpp c674033 c674032)
|
|> ((p X Y) <-- (pp X Y))
|=============================
|Step 18
|
|? (pp c674033 c674032)
|
|1. (~ (p c674033 c674032))
|2. (~ (p c674033 c674031))
|3. (p c674031 c674033)
|4. (~ (pp c674033 c674031))
|5. (e= c674032 c674031)
|6. (tpp c674033 c674032)
|
|> ((pp X Y) <-- (tpp X Y))
|=============================
|Step 19
|
|? (tpp c674033 c674032)
|
|1. (~ (pp c674033 c674032))
|2. (~ (p c674033 c674032))
|3. (~ (p c674033 c674031))
|4. (p c674031 c674033)
|5. (~ (pp c674033 c674031))
|6. (e= c674032 c674031)
|7. (tpp c674033 c674032)
|
|> hyp
=============================
Step 20

? (~ (e= c674031 c674033))

1. (p c674031 c674033)
2. (~ (pp c674033 c674031))
3. (e= c674032 c674031)
4. (tpp c674033 c674032)

> ((~ (e= X Z)) <-- (p Y X) (~ (p Y Z)))
|=============================
|Step 21
|
|? (p Var96 c674031)
|
|1. (e= c674031 c674033)
|2. (p c674031 c674033)
|3. (~ (pp c674033 c674031))
|4. (e= c674032 c674031)
|5. (tpp c674033 c674032)
|
|> ((p X Y) <-- (e= X Y))
|=============================
|Step 22
|
|? (e= Var96 c674031)
|
|1. (~ (p Var96 c674031))
|2. (e= c674031 c674033)
|3. (p c674031 c674033)
|4. (~ (pp c674033 c674031))
|5. (e= c674032 c674031)
|6. (tpp c674033 c674032)
|
|> hyp
=============================
Step 23

? (~ (p c674032 c674033))

1. (e= c674031 c674033)
2. (p c674031 c674033)
3. (~ (pp c674033 c674031))
4. (e= c674032 c674031)
5. (tpp c674033 c674032)

> ((~ (p Y X)) <-- (pp X Y))
=============================
Step 24

? (pp c674033 c674032)

1. (p c674032 c674033)
2. (e= c674031 c674033)
3. (p c674031 c674033)
4. (~ (pp c674033 c674031))
5. (e= c674032 c674031)
6. (tpp c674033 c674032)

> ((pp X Y) <-- (tpp X Y))
=============================
Step 25

? (tpp c674033 c674032)

1. (~ (pp c674033 c674032))
2. (p c674032 c674033)
3. (e= c674031 c674033)
4. (p c674031 c674033)
5. (~ (pp c674033 c674031))
6. (e= c674032 c674031)
7. (tpp c674033 c674032)

> hyp


LEMMA

From tpp(x,y) and e=(y,z), transport the tangential witness to z.
=============================
Step 1

? (all x (all y (all z (((tpp x y) & (e= y z)) => (exists w ((ec w x) & (ec w z)))))))


> revsk
=============================
Step 2

? (exists x680039 ((((~ (tpp c680042 c680041)) v (~ (e= c680041 c680040))) v (ec x680039 c680042)) & (((~ (tpp c680042 c680041)) v (~ (e= c680041 c680040))) v (ec x680039 c680040))))


> eR
=============================
Step 3

? ((((~ (tpp c680042 c680041)) v (~ (e= c680041 c680040))) v (ec Var37 c680042)) & (((~ (tpp c680042 c680041)) v (~ (e= c680041 c680040))) v (ec Var37 c680040)))


> &r
|=============================
|Step 4
|
|? (((~ (tpp c680042 c680041)) v (~ (e= c680041 c680040))) v (ec (f674125 c680042 c680041) c680042))
|
|
|> hypdisj
|=============================
|Step 5
|
|? (ec (f674125 c680042 c680041) c680042)
|
|1. (e= c680041 c680040)
|2. (tpp c680042 c680041)
|
|> ((ec (f674125 X Y) X) <-- (tpp X Y))
|=============================
|Step 6
|
|? (tpp c680042 c680041)
|
|1. (~ (ec (f674125 c680042 c680041) c680042))
|2. (e= c680041 c680040)
|3. (tpp c680042 c680041)
|
|> hyp
=============================
Step 7

? (((~ (tpp c680042 c680041)) v (~ (e= c680041 c680040))) v (ec (f674125 c680042 c680041) c680040))


> hypdisj
=============================
Step 8

? (ec (f674125 c680042 c680041) c680040)

1. (e= c680041 c680040)
2. (tpp c680042 c680041)

> ((ec Y X) <-- (e= Z X) (ec Y Z))
|=============================
|Step 9
|
|? (e= Var51 c680040)
|
|1. (~ (ec (f674125 c680042 c680041) c680040))
|2. (e= c680041 c680040)
|3. (tpp c680042 c680041)
|
|> hyp
=============================
Step 10

? (ec (f674125 c680042 c680041) c680041)

1. (~ (ec (f674125 c680042 c680041) c680040))
2. (e= c680041 c680040)
3. (tpp c680042 c680041)

> ((ec (f674125 X Y) Y) <-- (tpp X Y))
=============================
Step 11

? (tpp c680042 c680041)

1. (~ (ec (f674125 c680042 c680041) c680041))
2. (~ (ec (f674125 c680042 c680041) c680040))
3. (e= c680041 c680040)
4. (tpp c680042 c680041)

> hyp


LEMMA

Use Lemma5 for pp(x,z) and Lemma6 for an ec witness shared by x and z; hence tpp(x,z).
=============================
Step 1

? (all x (all y (all z (((tpp x y) & (e= y z)) => (tpp x z)))))


> revsk
=============================
Step 2

? (((~ (tpp c686448 c686447)) v (~ (e= c686447 c686446))) v (tpp c686448 c686446))


> hypdisj
=============================
Step 3

? (tpp c686448 c686446)

1. (e= c686447 c686446)
2. (tpp c686448 c686447)

> ((tpp X Z) <-- (pp X Z) (ec Y X) (ec Y Z))
||=============================
||Step 4
||
||? (pp c686448 c686446)
||
||1. (~ (tpp c686448 c686446))
||2. (e= c686447 c686446)
||3. (tpp c686448 c686447)
||
||> ((pp X Z) <-- (tpp X Y) (e= Y Z))
|||=============================
|||Step 5
|||
|||? (tpp c686448 Var41)
|||
|||1. (~ (pp c686448 c686446))
|||2. (~ (tpp c686448 c686446))
|||3. (e= c686447 c686446)
|||4. (tpp c686448 c686447)
|||
|||> hyp
||=============================
||Step 6
||
||? (e= c686447 c686446)
||
||1. (~ (pp c686448 c686446))
||2. (~ (tpp c686448 c686446))
||3. (e= c686447 c686446)
||4. (tpp c686448 c686447)
||
||> hyp
|=============================
|Step 7
|
|? (ec (f680049 c686448 Var47 Var48) c686448)
|
|1. (~ (tpp c686448 c686446))
|2. (e= c686447 c686446)
|3. (tpp c686448 c686447)
|
|> ((ec (f680049 X Y Z) X) <-- (tpp X Y) (e= Y Z))
||=============================
||Step 8
||
||? (tpp c686448 Var47)
||
||1. (~ (ec (f680049 c686448 Var47 Var48) c686448))
||2. (~ (tpp c686448 c686446))
||3. (e= c686447 c686446)
||4. (tpp c686448 c686447)
||
||> hyp
|=============================
|Step 9
|
|? (e= c686447 Var48)
|
|1. (~ (ec (f680049 c686448 c686447 Var48) c686448))
|2. (~ (tpp c686448 c686446))
|3. (e= c686447 c686446)
|4. (tpp c686448 c686447)
|
|> hyp
=============================
Step 10

? (ec (f680049 c686448 c686447 c686446) c686446)

1. (~ (tpp c686448 c686446))
2. (e= c686447 c686446)
3. (tpp c686448 c686447)

> ((ec (f680049 X Y Z) Z) <-- (tpp X Y) (e= Y Z))
|=============================
|Step 11
|
|? (tpp c686448 c686447)
|
|1. (~ (ec (f680049 c686448 c686447 c686446) c686446))
|2. (~ (tpp c686448 c686446))
|3. (e= c686447 c686446)
|4. (tpp c686448 c686447)
|
|> hyp
=============================
Step 12

? (e= c686447 c686446)

1. (~ (ec (f680049 c686448 c686447 c686446) c686446))
2. (~ (tpp c686448 c686446))
3. (e= c686447 c686446)
4. (tpp c686448 c686447)

> hyp
